Nuprl Lemma : rv-compose_wf
11,40
postcript
pdf
p
:FinProbSpace,
n
:
,
X
:RandomVariable(
p
;
n
),
F
:(
). (
X
.
F
(
X
)) o
X
RandomVariable(
p
;
n
)
latex
Definitions
RandomVariable(
p
;
n
)
,
(
x
.
F
(
x
)) o
X
,
x
.
A
(
x
)
,
x
(
s
)
,
f
(
a
)
,
Type
,
{
i
..
j
}
,
#$n
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
Outcome
,
x
:
A
.
B
(
x
)
,
,
,
t
T
,
FinProbSpace
Lemmas
finite-prob-space
wf
,
nat
wf
,
rationals
wf
,
p-outcome
wf
,
int
seg
wf
origin
p:FinProbSpace, n:
, X:RandomVariable(p;n), F:(
). (X.F(X)) o X 
RandomVariable(p;n) p:FinProbSpace, n:, X:RandomVariable(p;n), F:(). (X.F(X)) o X RandomVariable(p;n) 
x.A(x)
}B(x)x:A. B(x) T